/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.Collections;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.ArrowMultExpr;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.ElemFormula;
import alloy.ast.EmptyExpr;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.Exprs;
import alloy.ast.Formula;
import alloy.ast.Function;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IntExpr;
import alloy.ast.IntExprCastExpr;
import alloy.ast.InvocablePara;
import alloy.ast.Invocation;
import alloy.ast.InvocationExpr;
import alloy.ast.InvocationFormula;
import alloy.ast.Let;
import alloy.ast.LetDecl;
import alloy.ast.LetFormula;
import alloy.ast.LetImpl;
import alloy.ast.ModuleInfo;
import alloy.ast.MultiplicityExpr;
import alloy.ast.MultiplicityFormula;
import alloy.ast.Node;
import alloy.ast.QualifiedName;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.ast.SumExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.ast.UniversalExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.type.UnionType;

/**
 * <p>
 * A visitor that performs typechecking on a subtree of the AST.  Each
 * <code>visit()</code> method attempts to typecheck the expression passed
 * in.  Also, some desugarings are performed, so the <code>visit()</code>
 * methods return either the original node or a replacement for it.  If any
 * kind of semantic error is detected, a
 * {@link ExprTypeCheckVisitor.TypeCheckException} is thrown.  The class
 * is used by calling the {@link #typecheckNode typecheckNode} method.
 */

public class ExprTypeCheckVisitor extends ASTDepthFirstReplacer {

    /**
     * current module info, used for typechecking constructs in
     * which only the module info for the enclosing module is necessary.
     */
    private ModuleInfo _moduleInfo;

    /** the LocalScope enclosing the expressions */
    private LocalScope _localScope;

    private Map /* String -> UnionType */ _skolemTypes;
    
    /**
     * TypeErrorReporter used by this ExprTypeCheckVisitor
     **/
    private TypeErrorReporter _err;

    /**
     * @param moduleInfo_ the current module info
     * @param localScope_ the current local scope
     */
    private ExprTypeCheckVisitor(ModuleInfo moduleInfo_,
				 LocalScope localScope_,
				 Map skolemTypes_,
				 TypeErrorReporter err_) {
        _moduleInfo = moduleInfo_;
        if (_moduleInfo == null) throw new NullPointerException();
        _localScope = localScope_;
        _skolemTypes = skolemTypes_;
	_err = err_;
    }

    /**
     * Typechecks an AST node.
     * @param node_  the AST node to be typechecked
     * @param moduleInfo_ the current module info
     * @param localScope_ the current local scope
     * @param skolemTypes_ maps skolem constant names to their types
     * @param err_ TypeErrorReporter to be used for error reporting
     * @return the typechecked and (if necessary) desugared version of node_
     * @throws TypeCheckException if a semantic error occurs
     **/
    public static Node typecheckNode(Node node_, ModuleInfo moduleInfo_,
            						   LocalScope localScope_, Map skolemTypes_,
            						   TypeErrorReporter err_) {
       
    	ExprTypeCheckVisitor etcv =
    	    new ExprTypeCheckVisitor(moduleInfo_, localScope_,  
    	                            skolemTypes_, err_);

    	node_ = (Node) node_.applyReturnVisitor(etcv);
    	
    	OverloadingResolutionVisitor orv =
    	    new OverloadingResolutionVisitor(moduleInfo_, localScope_, err_);

    	node_.applyVisitor(orv);

    	if (err_.getError())
    	    throw new TypeCheckException();

    	return node_;
    }
    

    /**
     * Typechecks an AST node.
     * @param node_  the AST node to be typechecked
     * @param moduleInfo_ the current module info
     * @param localScope_ the current local scope
     * @return the typechecked and (if necessary) desugared version of node_
     * @throws TypeCheckException if a semantic error occurs
     **/
    public static Node typecheckNode(Node node_,
                     ModuleInfo moduleInfo_,
                     LocalScope localScope_) {
        return typecheckNode(node_, moduleInfo_, localScope_, Collections.EMPTY_MAP, 
                             new TypeErrorReporter());
	
    }

    /**
     * Typechecks an AST node, using the specified skolem constants (used by {@link alloy.api.AlloyEvaluator}).
     * @param node_  the AST node to be typechecked
     * @param moduleInfo_ the current module info
     * @param localScope_ the current local scope
     * @return the typechecked and (if necessary) desugared version of node_
     * @throws TypeCheckException if a semantic error occurs
     **/
    public static Node typecheckNode(Node node_, 
				     ModuleInfo moduleInfo_,
				     LocalScope localScope_,
				     Map /* String->UnionType */ skolemTypes_) {

        return typecheckNode(node_, moduleInfo_, localScope_, skolemTypes_, 
                new TypeErrorReporter());
    }
    

    

    //*************//
    // EXPRESSIONS //
    //*************//

    /**
     * @return true if ut.size() == 0; false otherwise
     **/
    private static boolean zeroSized(UnionType ut) {
    return (ut.size() == 0);
    }

    /**
     * @param opAndReason String describing the operation and reason why it failed
     * (e.g. "union (arity mismatch)")
     * @return a String of the form "incompatible types for <opAndReason>"
     **/
    private static String _binOpError(String opAndReason) {
    return ("incompatible types for " + opAndReason);
    }

    /**
     * typecheck a binary expression
     * @param binaryExpr_ the expression
     */
    public Object visit(BinaryExpr binaryExpr_) {

	    UnionType retType = null;
	
	    Expr left = (Expr) binaryExpr_.getLeft().applyReturnVisitor(this);
	    binaryExpr_.setLeft(left);
	    UnionType leftType = left.getType();
	    
	    Expr right = (Expr) binaryExpr_.getRight().applyReturnVisitor(this);
	    binaryExpr_.setRight(right);
	    UnionType rightType = right.getType();
	
	    // indicates whether one or both subexpression of binaryExpr_ contain a type error
	    // which would have resulted in a zero-sized UnionType
	    boolean subExprError = (zeroSized(leftType) || zeroSized(rightType));
	
	    // for all of the operations below, we don't report any errors if one of the subexpressions
	    // already contains an error in order to avoid upward propagation of error reports
	    BinaryExprOp op = binaryExpr_.getOp();
	
	    // for +, the resulting type is the union of left type and right type if
	    // there exist r1 in leftType and r2 in rightType such that r1.arity() == r2.arity();
	    // otherwise, the resulting type is a zero-sized UnionType
	    if (op.equals(BinaryExprOp.UNION)) {
	        // if leftType and rightType contain no RelationTypes of same arity, this is an arity error
	        if (!subExprError && zeroSized(leftType.intersect(rightType))) {
	        _err.type(_binOpError("union (arity mismatch)"), binaryExpr_);
	        retType = new UnionType();
	        } else {
	        retType = leftType.union(rightType);
	        }
	    }
	
	    // for ++, the resulting type is the union of left type and right type if
	    // there exist r1 in leftType and r2 in rightType such that r1.arity() == r2.arity()
	    // and dom(r1) & dom(r2) is non-empty; otherwise, the resulting type is a zero-sized UnionType
	    else if (op.equals(BinaryExprOp.RELATIONALOVERRIDE)) {
	        if (!subExprError && !rightType.canOverride(leftType)) {
	        _err.type(_binOpError("relational override"), binaryExpr_);
	        retType = new UnionType();
	        } else {
	        retType = leftType.union(rightType);
	        }
	    }
	
	    // for - and &, the left and right type must have matching arities and their intersection
	    // must be non-empty; if this is the case, the resulting type is leftType for - and
	    // the intersection for &; otherwise, the resulting type is a zero-sized UnionType
	    else if (op.equals(BinaryExprOp.INTERSECT)) {
	        // for & and -, the left and right type must intersect
	        retType = leftType.intersect(rightType);
	        if (!subExprError && retType.isEmpty()) {
	        _err.type(_binOpError("intersection " +
	                      (zeroSized(retType) ?
	                       "(arity mismatch)" :
	                       "(types are disjoint)")),
	               binaryExpr_);
	
	        }
	
	    }
	
	    else if (op.equals(BinaryExprOp.DIFF)) {
	        if (!subExprError && leftType.intersect(rightType).isEmpty()) {
	        _err.type(_binOpError("difference (types are disjoint)"), binaryExpr_);
	        }
	        retType = leftType;
	    }
	
	    // for join, the resulting type is the relational join of the left and right types iff
	    // there exist r1 in leftType and r2 in rightType such that r1.arity() + r2.arity() > 2
	    // and range(r1) & dom(r2) is non-empty; otherwise, the resulting type is a zero-sized UnionType
	    else if (op.equals(BinaryExprOp.JOIN_DOT) || op.equals(BinaryExprOp.JOIN_DOUBLECOLON) ||
	            op.equals(BinaryExprOp.JOIN_SQBRACKETS)) {
	        retType = leftType.join(rightType);
	        if (!subExprError && zeroSized(retType)) {
	        _err.type(_binOpError("join"), binaryExpr_);
	        }
	    }
	
	    else if (op.equals(BinaryExprOp.RELATION)) {
	        retType = leftType.product(rightType);
	        if (!subExprError && zeroSized(retType)) {
	        _err.type(_binOpError("product (cannot combine empty and non-empty types)"),
	              binaryExpr_);
	        }
	    }
	
	    // for <:, the type is the domain restriction of the right type based on the left type;
	    // the resulting type has non-zero size if there exist r1 in leftType and r2 in rightType such that
	    // r1.arity() == 1 and r1 & dom(r2) is non-empty
	    else if (op.equals(BinaryExprOp.DOMAINRESTRICT)) {
	        retType = rightType.domainRestrict(leftType);
	
	        // if both types are non-empty and retType is empty, this is a restriction error
	        if (!subExprError && retType.isEmpty()) {
	        _err.type(_binOpError("domain restriction (left and domain(right) are disjoint)"),
	              binaryExpr_);
	        }
	
	    }
	
	    // for :>, the type is the range restriction of the left type based on the right type;
	    // the resulting type has non-zero size if there exist r1 in leftType and r2 in rightType such that
	    // r2.arity() == 1 and range(r1) & r2 is non-empty
	    else if (op.equals(BinaryExprOp.RANGERESTRICT)) {
	        retType = leftType.rangeRestrict(rightType);
	
	        // if both types are non-empty and retType is empty, this is a restriction error
	        if (!subExprError && retType.isEmpty()) {
	        _err.type(_binOpError("range restriction (range(left) and right are disjoint)"),
	              binaryExpr_);
	        }
	    }
	
	    else {
	        retType = new UnionType();
	        _err.syntax("unknown binary operator (\"" +
	            binaryExpr_.getOp().toString() + "\")", binaryExpr_);
	    }
	
	    
	    //System.out.println(" In visit binary expr " + binaryExpr_ + " retType " + retType);
	    binaryExpr_.setType(retType);
	    return binaryExpr_;
    }


    /**
     * type checks an arrow multiplicity expression.
     * this is done by type checking its left and right
     * expressions, and then appending the right type
     * to the left type to create a new UnionType
     * @param arrowMultExpr_ the expression
     */
    public Object visit(ArrowMultExpr arrowMultExpr_) {
        arrowMultExpr_.setLeft((MultiplicityExpr) arrowMultExpr_.getLeft().applyReturnVisitor(this));
        arrowMultExpr_.setRight((MultiplicityExpr) arrowMultExpr_.getRight().applyReturnVisitor(this));
	MultiplicityExpr left = arrowMultExpr_.getLeft();
	MultiplicityExpr right = arrowMultExpr_.getRight();
	UnionType leftType = left.getType();
        UnionType rightType = right.getType();
	UnionType retType = leftType.product(rightType);
	if (!zeroSized(leftType) && !zeroSized(rightType) && zeroSized(retType)) {
	    _err.type(_binOpError("multiplicity product "+
				  "(cannot combine empty and non-empty types)\n") +
				  TypeErrorReporter.format("Expression", arrowMultExpr_) +
				  TypeErrorReporter.format("\nLeft",  left) +
				  TypeErrorReporter.format("\nRight", right),
		      arrowMultExpr_);
	}
	arrowMultExpr_.setType(retType);
	return arrowMultExpr_;
    }

    /**
     * type checks a comprehension expression.
     * first, each of the variables declared in the
     * expression are typed, with previous variables'
     * types available for typing later variables.  then,
     * the formula is type checked, and a relation type
     * consisting of the types of all the variables is the
     * type of the expression as a whole.
     * @param comprehensionExpr_ the {@link ComprehensionExpr}
     */
    public Object visit(ComprehensionExpr comprehensionExpr_) {
        Object ret = visit((VarCreator) comprehensionExpr_);
        _checkComprehensionDecls(comprehensionExpr_);
        return ret;
    }

    /**
     * ensure that all declarations in a comprehension expression are
     * singleton-tuples
     */
    private void _checkComprehensionDecls(ComprehensionExpr compExpr_) {
        Iterator declIter = compExpr_.getDecls().getDeclIter();
	while (declIter.hasNext()) {
	    Decl decl = (Decl)declIter.next();
	    if (decl.isHigherOrder()) {
		// declaration is invalid
		_err.semantic("higher order declarations not allowed in comprehensions", decl);
	    }
	}
    }

    private UnionType _univType() {
	return _moduleInfo.getUniv().getUnionType();
    }

    private UnionType _idenType() {
	UnionType univ = _univType();
	return univ.product(univ);
    }
  
    public Object visit(EmptyExpr emptyExpr_) {
    emptyExpr_.setType(UnionType.empty(1));
    return emptyExpr_;
    }

    /**
     * Typecheck an empty set expression.
     * @param emptySetExpr_ the empty set expression to typecheck
     */
    public Object visit(EmptySetExpr emptySetExpr_) {
    visit((Node) emptySetExpr_);
    emptySetExpr_.setType(UnionType.empty(1));
    return emptySetExpr_;
    }

    /**
     * Typecheck a univeral expression.  Return SigExpr of type univ.
     * @param universalExpr_ the universal expression to typecheck
     */
    public Object visit(UniversalExpr universalExpr_) {
	/**	
	   visit((Node) universalExpr_);
	   universalExpr_.setType(UnionType.univ());
	**/
	SigExpr univSigExpr = new SigExpr(universalExpr_.getLocation(),
					  (QualifiedName) _moduleInfo.getUniv().getName().copy());
	univSigExpr.setType(_univType());
	return univSigExpr;
    }

    /**
     * Typecheck an identity expression.
     * @param identityExpr_ the identity expression to typecheck
     */
    public Object visit(IdentityExpr identityExpr_) {
	visit((Node) identityExpr_);
	identityExpr_.setType(_idenType());
	return identityExpr_;
    }

    /**
       type checks an if-then-else expression.  The type of the resulting IfThenElseExpr
       if the type of Then unioned with the type of Else.
    */
    public Object visit(IfThenElseExpr ifThenElseExpr_) {

        ifThenElseExpr_.setIfFormula(
                                     (Formula) ifThenElseExpr_.getIfFormula().applyReturnVisitor(this));
        ifThenElseExpr_.setThenExpr(
                                    (Expr) ifThenElseExpr_.getThenExpr().applyReturnVisitor(this));
        ifThenElseExpr_.setElseExpr(
                                    (Expr) ifThenElseExpr_.getElseExpr().applyReturnVisitor(this));
        Expr thenExpr = ifThenElseExpr_.getThenExpr();
    Expr elseExpr = ifThenElseExpr_.getElseExpr();
    UnionType thenType = thenExpr.getType();
        UnionType elseType = elseExpr.getType();
    if (!zeroSized(thenType) && !zeroSized(elseType) &&
        zeroSized(thenType.intersect(elseType))) {
        _err.type(_binOpError("if-then-else (arity mismatch)\n") +
                TypeErrorReporter.format((Expr)ifThenElseExpr_) +
                TypeErrorReporter.format("\nThen", thenExpr) +
                TypeErrorReporter.format("\nElse", elseExpr),
              ifThenElseExpr_);
    }
    ifThenElseExpr_.setType(thenType.union(elseType));
    return ifThenElseExpr_;
    }

    /**
     * type checks an invocation expression.
     * @param invocationExpr_ the invocation expression to be typechecked
     */
    public Object visit(InvocationExpr invocationExpr_) {
        // first, typecheck the invocation parameters
        _typecheckParams(invocationExpr_);

        // then, check that the invocable is defined
        InvocablePara invocable = _findInvocable(invocationExpr_);
        UnionType invExprType = new UnionType();

        // invocable is defined . . .
        if (invocable != null) {
            invocationExpr_.setInvocable(invocable);

            // check that this is not a predicate
            if (invocable instanceof alloy.ast.Predicate) {
                _err.invocation("cannot invoke a predicate as an expression",
                                (Invocation) invocationExpr_);
            } else {
                // now, create a list of the arguments (expressions)
                // to be passed to the invocable
                List invArgs = invocationExpr_.getArgs();
                List argTypes = invocable.getArgList().getArgTypes();

                // if the number of arguments doesn't match the number of formals,
                // signal an error
                if (invArgs.size() != argTypes.size()) {
                    // subtract 1 for result "argument" of functions
                    _err.invocation("improper number of arguments (expected " +
                        argTypes.size() + ")", (Invocation) invocationExpr_);
                } else {
                    _matchParamsToFormals(invArgs, argTypes);
                    invExprType = ((Function)invocable).getReturnDecl().getExpr().getType();
                }
            }
        }

        invocationExpr_.setType(invExprType);
        return invocationExpr_;
    }

     private InvocablePara _findInvocable(Invocation invocation_) {
        QualifiedName invocableName = invocation_.getInvocableName();
        InvocablePara invocable = _moduleInfo.getInvocable(invocableName, null);
        if (invocable == null) {
        _err.invocation("the invocable " +
                invocableName.nodeString() + " is undefined", invocation_);
    }
        return invocable;
    }

    /**
     * type check the parameters of an invocation.  Also ensure that types of all parameters
     * are resolved at the time of invocation.
     */
    private void _typecheckParams(Invocation invocation_) {
    // the expressions that are invocation parameters must have resolved types,
    // so we'll typecheck the left and right parts using a new ExprTypeCheckVisitor
    try {
        invocation_.setReceiver((Expr) typecheckNode(invocation_.getReceiver(),
                             _moduleInfo,
                             _localScope, _skolemTypes, 
                             new TypeErrorReporter(_err.getReport())));
    } catch (TypeCheckException rTCE) {
        invocation_.getReceiver().setType(new UnionType());
        _err.setError(true); // record the fact that we've seen an error
    }

    Exprs exprs = new Exprs();
    for (Iterator exprIter = invocation_.getExprs().getExprIter(); exprIter.hasNext() ;) {
        Expr curExpr = (Expr) exprIter.next();
        try {
        curExpr = (Expr) typecheckNode(curExpr,
                           _moduleInfo, _localScope, _skolemTypes,
                           new TypeErrorReporter(_err.getReport()));
        } catch (TypeCheckException eTCE) {
        curExpr.setType(new UnionType());
        _err.setError(true); // record the fact that we've seen an error
        }
        exprs.addExpr(curExpr);
    }
    invocation_.setExprs(exprs);
    }

    /**
     * ensure that the parameter types of an invocation
     * are consistent with the types of the formals of the function.
     * @param funArgs_ the argument expressions of the invocation
     * @param formalTypes_ the argument types of the function
     */
    private void _matchParamsToFormals(List funArgs_, List formalTypes_) {
    // iterate through the arguments and formal types
        for (int i = 0; i < funArgs_.size(); i++) {

        // all arguments have union types assigned to them (ambiguously typed
        // expressions cannot be passed in to or returned by functions)
            Expr curArg = (Expr) funArgs_.get(i);

            UnionType curArgType = curArg.getType();
        UnionType curFormalType = (UnionType) formalTypes_.get(i);

        // now, see if argument type matches formal type
        if (!argTypeMatchesFormalType(curArgType, curFormalType)) {
                _err.invocation("incompatible formal and actual types for invocation" +
				(curArgType.arity()==curFormalType.arity() ? "\n" :
				 " (arity mismatch)\n") +
				 TypeErrorReporter.format(curArg) +
				"\nExpected type: " + curFormalType.toString(),
				curArg);
        }
        }
    }

    /**
     * see if an argument type and a formal type are compatible.
     * @param argType_ the argument type
     * @param formalType_ the type of the formal
     * @return <code>true</code> if the types match; <code>false</code> otherwise
     */
    private static boolean argTypeMatchesFormalType(UnionType argType_,
                            UnionType formalType_) {
    return (zeroSized(argType_) || 
	    ((argType_.isEmpty() || formalType_.isEmpty()) && 
	     (argType_.arity() == formalType_.arity())) ||
	    !argType_.intersect(formalType_).isEmpty());

    }


    /**
     * type check a set multiplicity expression by
     * type checking the expression qualified by the
     * multiplicity
     * @param setMultExpr_ the SetMultExpr
     */
    public Object visit(SetMultExpr setMultExpr_) {
        setMultExpr_.setExpr((Expr)setMultExpr_.getExpr().applyReturnVisitor(this));
    // give the setMultExpr_ the type of its child
    setMultExpr_.setType(setMultExpr_.getExpr().getType());
    return setMultExpr_;
    }

    /**
     * type check a SigExpr
     * @param sigExpr_ the SigExpr
     */
    public Object visit(SigExpr sigExpr_) {
        // call a helper function to type check the sig. expr.
	//System.out.println("visiting " + sigExpr_.nodeString());
        return typecheckSigExpr(sigExpr_);
    }

    /**
     * Helper function for type checking sig. exprs.
     * @param sigExpr_ the SigExpr to be typechecked
     */
    private SigExpr typecheckSigExpr(SigExpr sigExpr_) {

        if (sigExpr_.getType() != null) {
          return sigExpr_;
        }
        
	SigExpr replacement = sigExpr_;
	UnionType replacementType = null;
	
	
	// first, get the signature
	Signature sig = _moduleInfo.getSignature(sigExpr_.getSig(), "reference");
	
	// if no signature is found, give sigExpr_ the zero sized UnionType
	if (sig == null) {
	    replacement = sigExpr_;
	    replacementType = new UnionType();
	} else {
	    // replace sig expr with new sig expr that uses fully qualified name
	    replacement =
            new SigExpr(sigExpr_.getLocation(), sig.getName());
	    // give the replacement the type of the sig
	    replacementType = sig.getUnionType();
	}
	
	replacement.setType(replacementType);
	return replacement;
    }

    /** Visit a node of type {@link UnaryExpr}
     *  and traverse its children depth first*/
    public Object visit(UnaryExpr unaryExpr_) {
        UnaryExprOp op = unaryExpr_.getOp();
	    unaryExpr_.setExpr((Expr)unaryExpr_.getExpr().applyReturnVisitor(this));
	
	    Expr expr = unaryExpr_.getExpr();
	    UnionType exprType = expr.getType();
	    UnionType retType;
	
	    // if ExprType is not zero-sized and doesn't contain at least one RelationType of arity 2,
	    // signal an error
	    if (!exprType.hasArity(2)) {
	        retType = new UnionType();
	        if (!zeroSized(exprType)) {
		    _err.type("improper type for a unary operation (expression must have arity 2)\n"+
		            TypeErrorReporter.format(expr), expr);
	        }
	    } else {
	
	        if (op.equals(UnaryExprOp.TRANSPOSE)) {
		        // for transpose, just create a new UnionType
		        // that is the transpose of the type of expr
		        retType = exprType.transpose();
	        } else {
		        // first, compute the closure type
		        retType = exprType.closure();
		        //make sure that the closure type is not
		        // just a subset of exprType
		        if (zeroSized(retType.join(retType))) {
		            _err.semantic("redundant closure operation (domain and range are disjoint)\n"+
		                    TypeErrorReporter.format(expr), expr);
		        }
		        // if this is reflexive transitive closure, add iden to the result
		        if (op.equals(UnaryExprOp.REF_TRANS_CLOSURE)) {
		            retType = retType.union(_idenType());
		        }
	        }
	    }
	
	    unaryExpr_.setType(retType);

        return unaryExpr_;
    }

    /**
     * Typecheck a variable expression.  First, check if the variable is bound in the
     * local scope, and if so get its type from the scope.  Next, if the variable is the
     * name of a field, give it the same type as the type of the field.  If none of the
     * aformentioned attempts successfully type the variable, produce an error.
     * @param variableExpr_ the VariableExpr
     */
    public Object visit(VariableExpr variableExpr_) {
	// do nothing if the variableExpr_ is already typed 
	// this case will arise when we are using the typechecker
	// to "minimize" the types of inlined function/predicate
	// expressions (see alloy.transform.InvocationInlineVisitor)

	if (variableExpr_.getType() != null)
	    return variableExpr_;

    String varString = variableExpr_.getVar().getId().nodeString();
    // see if the variable is bound in the local scope
    UnionType retType = _localScope.lookupType(varString);
    if (retType == null) {
	// is it a skolem constant?
	if (_skolemTypes != null)
	    retType = (UnionType)_skolemTypes.get(varString);
	if (retType == null) {
	    // try to type the VariableExpr as though it's a field
	    retType = new UnionType();
	    try {
		// get all signatures which have a field with the name varString and
		// set retType to be the union of types of all obtained fields
		for (Iterator sigIter = _moduleInfo.getSigsForField(varString).iterator();
		     sigIter.hasNext(); ) {
		    Signature sigWithField = (Signature) sigIter.next();
		    UnionType uType = sigWithField.getFieldType(varString);
		    if (uType != null)
			retType = retType.union(uType);
		}
		// there are sigs with this field name, but we could not determine the field's
	    // type -- this would happen if we had a declaration of the form
	    // sig A { a : a}
	    if (retType.isEmpty()) {
	        _err.type("unable to type variable " + variableExpr_, variableExpr_);
	    }
	    } catch (ModuleInfo.NoSigsException nse) {
		// couldn't type the variable as a field either
		_err.type("unable to type variable " + variableExpr_, variableExpr_);
	    }
	    
	}
    }
    
    variableExpr_.setType(retType);
    //System.out.println("typing variable " + variableExpr_ + " at " + retType);
    return variableExpr_;

    }


    //*****************//
    // INT EXPRESSIONS //
    //*****************//

    /**
     * Typecheck an int expr cast expr.  This type of
     * expression just has the type "Int".
     * @param intExprCastExpr_ the IntExprCastExpr
     */
    public Object visit(IntExprCastExpr intExprCastExpr_) {
        intExprCastExpr_.setIntExpr((IntExpr)intExprCastExpr_.getIntExpr().applyReturnVisitor(this));
	intExprCastExpr_.setType(_moduleInfo.getInt().getUnionType());
	return intExprCastExpr_;
    }

    /**
     * Typecheck an expr cast int expr.  The type of
     * the expr must be "Int".
     * @param exprCastIntExpr_ the ExprCastIntExpr
     * @return <code>exprCastIntExpr_</code> if no type-checking error occurs; otherwise <code>null</code>
     */
    public Object visit(ExprCastIntExpr exprCastIntExpr_) {
        exprCastIntExpr_.setExpr(_getIntTypedExpr(exprCastIntExpr_.getExpr()));
    // make sure that the type of expr is non-empty -- if it isn't,
    // we know that's a type error (see the spec of _getIntTypedExpr)
    Expr expr = exprCastIntExpr_.getExpr();
    if (expr.getType().isEmpty()) {
        _err.type("improper type for cast (expression must have type Int)\n" +
                TypeErrorReporter.format(expr), expr);
    }
        return exprCastIntExpr_;
    }

    /**
     * Typecheck a sumintexpr.  Create a local scope holding
     * all of its declared variables while typechecking their
     * declarations, and then typecheck the body.
     */
    public Object visit(SumIntExpr sumIntExpr_) {
        return visit((VarCreator) sumIntExpr_);
    }

    /**
       Typecheck a sum expression.  the expression must
       have type "Int".
    */
    public Object visit(SumExpr sumExpr_) {
        sumExpr_.setExpr(_getIntTypedExpr(sumExpr_.getExpr()));
        // make sure that the type of expr is non-empty -- if it isn't,
    // we know that's a type error (see the spec of _getIntTypedExpr)
    Expr expr = sumExpr_.getExpr();
        if (expr.getType().isEmpty()) {
            _err.type("improper type for sum (expression must have type Int)\n" +
                    TypeErrorReporter.format(expr), expr);
    }
        return sumExpr_;
    }

    /**
     * @return expr typechecked.  If the type of expr intersects with IntType, then
     * expr is given IntType.  Otherwise, expr is given zero-sized UnionType
     **/
    private Expr _getIntTypedExpr(Expr expr) {
    expr = (Expr) expr.applyReturnVisitor(this);
    UnionType intType = _moduleInfo.getInt().getUnionType();
    if (expr.getType().intersect(intType).isEmpty()) {
        expr.setType(new UnionType());
    } else {
        expr.setType(intType);
    }

    return expr;
    }

    //**********//
    // LET     //
    //**********//


    public Object visit(LetImpl letImpl_) {
    return _visitLet(letImpl_);
    }

    public Object visit(LetFormula letForm_) {
        return _visitLet(letForm_);
    }

    public Object _visitLet(Let let_) {

    // create a new LocalScope whose parent is current LocalScope
        LocalScope newScope = new LocalScope();
        newScope.addParent(_localScope);

        // iterate through decls
        Iterator declIter = let_.getLetDecls().getLetDeclIter();

    // flag that indicates whether it's ok to perform the desugaring or not:
    // if any errors are encountered during typechecking, we won't desugar the let,
    // otherwise we will
    boolean desugar = true;
        while (declIter.hasNext()) {
            LetDecl curDecl = (LetDecl) declIter.next();
            // typecheck next decl with newScope so it sees previous bindings; the type of
	    // the expression must be resolved.  If we encounter any errors while typechecking
	    // the declarations, we just set the type of that variable to zero-sized UnionType
        Expr curExpr = curDecl.getExpr();
        try {
	    curExpr = (Expr) typecheckNode(curExpr,
                           _moduleInfo, newScope, _skolemTypes,
                           new TypeErrorReporter(_err.getReport()));
        } catch (TypeCheckException tce) {
        curExpr.setType(new UnionType());
        desugar = false;
        }
        curDecl.setExpr(curExpr);

        try {
        newScope.addMapping(curDecl.getVar().getId().nodeString(),
                    curDecl.getExpr().getType());
        } catch (AlreadyMappedException ame) {
        _err.semantic("duplicate name declaration (variable "+
                  curDecl.getVar().getId().nodeString()+")", curDecl);
        desugar = false;
        }
        }

    // typecheck the body using the local scope
    Node body = let_.getBody();
    try {
        body = typecheckNode(body, _moduleInfo, newScope, _skolemTypes,
                new TypeErrorReporter(_err.getReport()));
    } catch (TypeCheckException bTCE) {
        desugar = false;
        if (body instanceof Expr)
        ((Expr) body).setType(new UnionType());
    }

    if (let_ instanceof LetFormula)
        ((LetFormula)let_).setBody(body);
    else
        ((LetImpl)let_).setBody(body);

    // if everything typechecked, desugar the body and return it
    /**
    if (desugar)
        return let_.applyReturnVisitor(new DesugarLetVisitor());
    else { // otherwise, record the fact that we've seen an error and return this let as is
        _err.setError(true);
        return let_;
    }
    **/

    if (!desugar) _err.setError(true);
    return let_;

    }
    //**********//
    // FORMULAS //
    //**********//

    /**
     * We visit Formulas to make sure that type checking is not aborted when
     * one of the formulas in the group has a type error.  Since no type information
     * is shared across formulas, it makes sense to continue type-checking
     * the remaining formulas once an error is encountered in one of the formulas
     **/
    /**
    public Object visit(Formulas formulas_) {

    Formulas retFormulas = new Formulas(formulas_.getLocation());
    Iterator formulaIter = formulas_.getFormulaIter();

    while (formulaIter.hasNext()) {
        retFormulas.addFormula((Formula) ((Formula) formulaIter.next()).applyReturnVisitor(this));
    }
        return retFormulas;

    }
    **/
    /**
     * type check an elementary formula (expr compop expr).  Make
     * sure that both expressions have intersecting types.
     * @param elemFormula_ the elementary formula to typecheck
     * @return <code>elemFormula_</code> if it typechecks properly; <code>null</code> otherwise
     */
    public Object visit(ElemFormula elemFormula_) {

    Expr left = (Expr) elemFormula_.getLeft().applyReturnVisitor(this);
    elemFormula_.setLeft(left);
    UnionType leftType = left.getType();
    
    Expr right = (Expr) elemFormula_.getRight().applyReturnVisitor(this);
    elemFormula_.setRight(right);
    UnionType rightType = right.getType();

    UnionType intersection = leftType.intersect(rightType);
    if ((!zeroSized(leftType) && !zeroSized(rightType) && zeroSized(intersection)) || 
        (!leftType.isEmpty() && !rightType.isEmpty() && intersection.isEmpty())) {
        _err.type(_binOpError(" subset (types are disjoint)\n") +
                TypeErrorReporter.format("Formula", elemFormula_) +
                TypeErrorReporter.format("\nLeft", elemFormula_.getLeft()) +
                TypeErrorReporter.format("\nRight", elemFormula_.getRight()), elemFormula_);
    }
    
    

    left.setType(leftType);
    if (elemFormula_.getOp().equals(CompOp.EQUALS) ||
            elemFormula_.getOp().equals(CompOp.EQUALS.negation())) {
    	  right.setType(rightType);
     } else {
        ///      catches the redundant constraint of the form "none in X"
        if (leftType.isEmpty() && !zeroSized(leftType) && !zeroSized(rightType) ) {
            _err.type("redundant constraint (left type is empty)\n" + 
                    TypeErrorReporter.format("Formula", elemFormula_) +
                    TypeErrorReporter.format("\nLeft", elemFormula_.getLeft()) +
                    TypeErrorReporter.format("\nRight", elemFormula_.getRight()), elemFormula_);
        }
	right.setType(intersection);
    }

    
    
    return elemFormula_;
    }

    /**
     * type check a multiplicity formula (expr : multiplicityExpr).  Make
     * sure that both expressions have intersecting types.
     * @param elemFormula_ the elementary formula to typecheck
     * @return <code>elemFormula_</code> if it typechecks properly; <code>null</code> otherwise
     */
    public Object visit(MultiplicityFormula multFormula_) {
	Expr left = (Expr) multFormula_.getLeft().applyReturnVisitor(this);
	multFormula_.setLeft(left);
	UnionType leftType = left.getType();
	
	MultiplicityExpr right = (MultiplicityExpr)
	    multFormula_.getRight().applyReturnVisitor(this);
	multFormula_.setRight(right);
	UnionType rightType = right.getType();
	
	UnionType intersection = leftType.intersect(rightType);
	
	if (!leftType.isEmpty() && !rightType.isEmpty() && intersection.isEmpty()) {
	    _err.type(_binOpError(" subset (types are disjoint)\n") +
	            TypeErrorReporter.format("Formula", multFormula_) +
	            TypeErrorReporter.format("\nLeft", multFormula_.getLeft()) +
	            TypeErrorReporter.format("\nRight", multFormula_.getRight()), multFormula_);
	}

	left.setType(leftType);
	right.setType(intersection);

	return multFormula_;

    }

    /**
     * type check an invocation formula.
     * @param invocationFormula_ the invocation formula to typecheck
     * @return <code>invocationFormula_</code> if it correctly typechecks; <code>null</code> otherwise
     */
    public Object visit(InvocationFormula invocationFormula_) {

    // first, typecheck the invocation parameters
    _typecheckParams(invocationFormula_);

    // then, check that the invocable is defined
    InvocablePara invocable = _findInvocable(invocationFormula_);

    // invocable is defined . . .
    if (invocable != null) {
        invocationFormula_.setInvocable(invocable);

        // check that this is not a function
        if (invocable instanceof alloy.ast.Function) {
        _err.invocation("cannot invoke a function as a formula",
                (Invocation) invocationFormula_);
        } else {
        // now, create a list of the arguments (expressions)
        // to be passed to the invocable
        List invArgs = invocationFormula_.getArgs();
        List argTypes = invocable.getArgList().getArgTypes();

        // if the number of arguments doesn't match the number of formals,
        // signal an error
        if (invArgs.size() != argTypes.size()) {
            _err.invocation("improper number of arguments (expected "+
                    argTypes.size() + ")", (Invocation) invocationFormula_);
        } else { //otherwise, check that types of args and formals intersect
            _matchParamsToFormals(invArgs, argTypes);
        }
        }
    }

    return invocationFormula_;
    }

    /**
     * Typecheck a quantified formula.  Get the types of
     * all the declared variables and bind them in a new
     * local scope.  Then, type check the formula body
     * with the new local scope.
     * @param quantifiedFormula_ the quantified formula to typecheck
     * @return <code>quantifiedFormula_</code> if it typechecks properly; <code>null</code> otherwise
     */
    public Object visit(QuantifiedFormula quantifiedFormula_) {
        return visit((VarCreator) quantifiedFormula_);
    }

    private Object visit(VarCreator creator_) {

        // create a new LocalScope whose parent is current LocalScope
        LocalScope newScope = new LocalScope();
        newScope.addParent(_localScope);

        // iterate through decls
        Iterator declIter = creator_.getDecls().getDeclIter();
        UnionType retType = null;

        while (declIter.hasNext()) {
            Decl curDecl = (Decl) declIter.next();
            // typecheck next decl with newScope so it sees previous bindings; the type of
        // the expression must be resolved.  If we cannot determine the type of current expression,
        // we'll give it a zero-sized UnionType
        MultiplicityExpr curExpr = curDecl.getExpr();
        try {
        curExpr = (MultiplicityExpr)
            typecheckNode(curExpr, _moduleInfo, newScope, _skolemTypes, 
                    	     new TypeErrorReporter(_err.getReport()));
        } catch (TypeCheckException tce) {
        curExpr.setType(new UnionType());
        _err.setError(true); // record the fact that we've seen an error
        }

        curDecl.setExpr(curExpr);

        UnionType curDeclType = curExpr.getType();


            Iterator varIter = curDecl.getVariables().getVariableIter();
            while (varIter.hasNext()) {
                Variable curVar = (Variable) varIter.next();
                try {
                    newScope.addMapping(curVar.getId().nodeString(), curDeclType);
                } catch (AlreadyMappedException ame) {
                    _err.semantic("duplicate name declaration (variable " +
                  curVar.getId().nodeString()+")", curDecl);
        }

                retType = (retType == null ? curDeclType : retType.product(curDeclType));
            }
        }
        // store the local scope
        creator_.setLocalScope(newScope);

    // typecheck the body
    try {
        creator_.setBody(typecheckNode(creator_.getBody(),
                        _moduleInfo, newScope, _skolemTypes,
                        new TypeErrorReporter(_err.getReport())));
    } catch (TypeCheckException bTCE) {
        _err.setError(true); // record the fact that we've seen an error
    }

        if (creator_ instanceof ComprehensionExpr) {
        ((ComprehensionExpr) creator_).setType(retType);
        }

    return creator_;
    }

    public static class TypeCheckException extends RuntimeException {}
}
